package no.uio.ifi.cop.prover.simple;

import java.util.Stack;
import java.util.TreeSet;
import java.util.Comparator;

import no.uio.ifi.cop.prover.RuleFinder;
import no.uio.ifi.cop.cl.Axiom;
import no.uio.ifi.cop.cl.Predicate;
import no.uio.ifi.cop.util.Tuple;
import no.uio.ifi.cop.cl.Substitution;
import no.uio.ifi.cop.common.Log;

import no.uio.ifi.cop.prover.RuleMatcher;

/**
 * SimpleRuleFinder is an example implementation of
 * the RuleFinder interface.
 *
 * @version 1.0
 * @author  bjarneh@ifi.uio.no
 */

public final class SimpleRuleFinder implements RuleFinder, Cloneable{

    static boolean dynamic; // that's a pretty good name static dynamic..
    TreeSet<SimpleRuleMatcher> rules;

    public SimpleRuleFinder(){
        this(null, false);
    }

    public SimpleRuleFinder(boolean dyn){
        this(null, dyn);
    }

    public SimpleRuleFinder( Comparator<? super RuleMatcher> c){
        this(c, false);
    }

    public SimpleRuleFinder( Comparator<? super RuleMatcher> c, boolean dyn){
        rules = new TreeSet<SimpleRuleMatcher>( c );
        dynamic = dyn;
    }

    // for cloning purposes..
    private SimpleRuleFinder( TreeSet<SimpleRuleMatcher> cpRules ){
        rules = cpRules;
    }

    public boolean exhausted(){
        if( next(false) == null ){
            resetAll();
            return (next(false) == null);
        }
        return false;
    }

    public void addRule(Axiom ax){
        Log.debug("addRule( %s )", ax);
        rules.add( new SimpleRuleMatcher( ax ) );
    }

    public Tuple<Axiom, Substitution> getNextMatch(){
        return next(true);
    }

    private void resetAll(){
        for(SimpleRuleMatcher rlm : rules ){ rlm.reset(); }
    }

    // concurrency problem, even with 2 threads things can get funky :-)
    private synchronized void stopOrReorder(SimpleRuleMatcher rlmatcher){
        if( rlmatcher == null ){
            for(SimpleRuleMatcher rlm : rules ){rlm.stop();}
        }else{
            rules.remove( rlmatcher );
            rules.add( rlmatcher );
        }
    }

    public void stop(){
        stopOrReorder( null );
    }

    private Tuple<Axiom, Substitution> next(boolean advance){

        Substitution subst;
        SimpleRuleMatcher rlmatcher = null;
        Tuple<Axiom, Substitution> pair = null;

        for( SimpleRuleMatcher rlm : rules ){
            subst = rlm.getNextMatch(advance);
            if( subst != null ){
                if( advance ){ rlm.advance();  }
                pair = new Tuple<Axiom, Substitution>( rlm.getAxiom(), subst );
                rlmatcher = rlm;
                break;
            }
        }

        // resort treeset by removing and adding
        // look ugly but that's the way to do it
        if( dynamic && pair != null ){
            stopOrReorder( rlmatcher );
///             rules.remove( rlmatcher );
///             rules.add( rlmatcher );
        }
        
        return pair;
    }

    public void addPredicate(Predicate p){
        for( SimpleRuleMatcher rlm : rules ){
            rlm.match( p );
        }
    }

    public RuleFinder clone(){

        TreeSet<SimpleRuleMatcher> copy =
            new TreeSet<SimpleRuleMatcher>( rules.comparator() );

        for( SimpleRuleMatcher rlm : rules ){
            copy.add( rlm.clone() );
        }

        return new SimpleRuleFinder( copy );
    }

    public String toString(){
        StringBuilder sb = new StringBuilder();
        sb.append("@SimpleRuleFinder\n");
        for( SimpleRuleMatcher rlm : rules ){
            sb.append(rlm.toString()).append("\n");
        }
        return sb.toString();
    }

}
